FDL - Nuprl Lemma : p-compose-inject

Nuprl Lemma : p-compose-inject

A, B, C:Type, g:(A

(B + Top)), f:(B

(C + Top)).
p-inject(A;B;g)

p-inject(B;C;f)

p-inject(A;C;f o g )

Definitions x:A. B(x), P & Q, P Q, {T}, s = t, b, p-inject(A;B;f), Top, left + right, x:AB(x), Type

Lemmas do-apply-compose, can-apply-compose